T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} ,
t:rationals. (x unchanged-for t @ e)  prop{i:l} 

latex

Definitions	Type, t  T, x:A. B(x), EqDecider(T), event_system{i:l}, Id, loc(e), es-dtype(es; i; x; T), es-E(es), {x:A| B(x)} , rationals, x:AB(x), es-time(es; e), P  Q, (last change to x before e), r + s, qle(r; s), x changed before e, b, prop{i:l}, (x unchanged-for t @ e)
Lemmas	assert wf, changed wf, qle wf, qadd wf, last-change wf, es-time wf, rationals wf, es-E wf, es-dtype wf, es-loc wf, Id wf, event system wf, deq wf